strict_part(x,y.R(x;y);a;b) == R(a;b) & (R(b;a)) 

latex

Definitions	P & Q, A
FDL editor aliases	strict_part